A, B:Realizer. A  B  (es:ES. Consistent(B;es)  Consistent(A;es)) 

latex

Definitions	x:A. B(x), P  Q, t  T, Prop, SQType(T), {T}, AB, A, False, ij, Consistent(R;es), True, P & Q, A  B, , Y, if b t else f fi, P  Q, true, false, P  Q,
Lemmas	nat wf, R-size wf, R-consistent wf, event system wf, R-sub wf, le wf, nat plus wf, es realizer wf, bool cases, Rnone? wf, bool sq, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, nat properties, ge wf, Rnone?-implies, Rplus? wf, R-size-decreases, Rplus-implies, Rplus-left wf, Rplus-right wf